YES(O(1),O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, -(@x, @y) -> #sub(@x, @y)
, div(@x, @y) -> #div(@x, @y)
, eratos(@l) -> eratos#1(@l)
, eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs)))
, eratos#1(nil()) -> nil()
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs' }
Weak Trs:
{ #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0()
, #natsub(@x, #0()) -> @x
, #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add following dependency tuples:
Strict DPs:
{ #equal^#(@x, @y) -> c_1(#eq^#(@x, @y))
, *^#(@x, @y) -> c_2(#mult^#(@x, @y))
, -^#(@x, @y) -> c_3(#sub^#(@x, @y))
, div^#(@x, @y) -> c_4(#div^#(@x, @y))
, eratos^#(@l) -> c_5(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, eratos#1^#(nil()) -> c_7()
, filter^#(@p, @l) -> c_8(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs))
, filter#1^#(nil(), @p) -> c_10()
, filter#2^#(@xs', @p, @x) ->
c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'),
#equal^#(mod(@x, @p), #0()),
mod^#(@x, @p))
, filter#3^#(#false(), @x, @xs') -> c_13()
, filter#3^#(#true(), @x, @xs') -> c_14()
, mod^#(@x, @y) ->
c_12(-^#(@x, *(@y, div(@x, @y))),
*^#(@y, div(@x, @y)),
div^#(@x, @y)) }
Weak DPs:
{ #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_16()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_17()
, #eq^#(nil(), nil()) -> c_18()
, #eq^#(#0(), #0()) -> c_19()
, #eq^#(#0(), #s(@y)) -> c_20()
, #eq^#(#0(), #neg(@y)) -> c_21()
, #eq^#(#0(), #pos(@y)) -> c_22()
, #eq^#(#s(@x), #0()) -> c_23()
, #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y))
, #eq^#(#neg(@x), #0()) -> c_25()
, #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y))
, #eq^#(#neg(@x), #pos(@y)) -> c_27()
, #eq^#(#pos(@x), #0()) -> c_28()
, #eq^#(#pos(@x), #neg(@y)) -> c_29()
, #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y))
, #mult^#(#0(), #0()) -> c_31()
, #mult^#(#0(), #neg(@y)) -> c_32()
, #mult^#(#0(), #pos(@y)) -> c_33()
, #mult^#(#neg(@x), #0()) -> c_34()
, #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_37()
, #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y))
, #sub^#(@x, #0()) -> c_40()
, #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y)))
, #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y)))
, #div^#(#0(), #0()) -> c_43()
, #div^#(#0(), #neg(@y)) -> c_44()
, #div^#(#0(), #pos(@y)) -> c_45()
, #div^#(#neg(@x), #0()) -> c_46()
, #div^#(#neg(@x), #neg(@y)) ->
c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#neg(@x), #pos(@y)) ->
c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #0()) -> c_49()
, #div^#(#pos(@x), #neg(@y)) ->
c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #pos(@y)) ->
c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #and^#(#false(), #false()) -> c_65()
, #and^#(#false(), #true()) -> c_66()
, #and^#(#true(), #false()) -> c_67()
, #and^#(#true(), #true()) -> c_68()
, #natmult^#(#0(), @y) -> c_85()
, #natmult^#(#s(@x), @y) ->
c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y))
, #add^#(#0(), @y) -> c_52()
, #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #positive^#(#0()) -> c_73()
, #positive^#(#s(@x)) -> c_74()
, #positive^#(#neg(@x)) -> c_75()
, #positive^#(#pos(@x)) -> c_76()
, #natdiv^#(#0(), #0()) -> c_69()
, #natdiv^#(#0(), #s(@y)) -> c_70()
, #natdiv^#(#s(@x), #0()) -> c_71()
, #natdiv^#(#s(@x), #s(@y)) ->
c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y))
, #negative^#(#0()) -> c_77()
, #negative^#(#s(@x)) -> c_78()
, #negative^#(#neg(@x)) -> c_79()
, #negative^#(#pos(@x)) -> c_80()
, #pred^#(#0()) -> c_57()
, #pred^#(#neg(#s(@x))) -> c_58()
, #pred^#(#pos(#s(#0()))) -> c_59()
, #pred^#(#pos(#s(#s(@x)))) -> c_60()
, #succ^#(#0()) -> c_61()
, #succ^#(#neg(#s(#0()))) -> c_62()
, #succ^#(#neg(#s(#s(@x)))) -> c_63()
, #succ^#(#pos(#s(@x))) -> c_64()
, #natdiv'^#(#0(), @y) -> c_89()
, #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y))
, #natdiv'^#(#underflow(), @y) -> c_91()
, #divsub^#(#0(), #0()) -> c_81()
, #divsub^#(#0(), #s(@y)) -> c_82()
, #divsub^#(#s(@x), #0()) -> c_83()
, #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y))
, #natadd^#(#0(), @y) -> c_87()
, #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y))
, #natsub^#(@x, #0()) -> c_92()
, #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ #equal^#(@x, @y) -> c_1(#eq^#(@x, @y))
, *^#(@x, @y) -> c_2(#mult^#(@x, @y))
, -^#(@x, @y) -> c_3(#sub^#(@x, @y))
, div^#(@x, @y) -> c_4(#div^#(@x, @y))
, eratos^#(@l) -> c_5(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, eratos#1^#(nil()) -> c_7()
, filter^#(@p, @l) -> c_8(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs))
, filter#1^#(nil(), @p) -> c_10()
, filter#2^#(@xs', @p, @x) ->
c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'),
#equal^#(mod(@x, @p), #0()),
mod^#(@x, @p))
, filter#3^#(#false(), @x, @xs') -> c_13()
, filter#3^#(#true(), @x, @xs') -> c_14()
, mod^#(@x, @y) ->
c_12(-^#(@x, *(@y, div(@x, @y))),
*^#(@y, div(@x, @y)),
div^#(@x, @y)) }
Weak DPs:
{ #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_16()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_17()
, #eq^#(nil(), nil()) -> c_18()
, #eq^#(#0(), #0()) -> c_19()
, #eq^#(#0(), #s(@y)) -> c_20()
, #eq^#(#0(), #neg(@y)) -> c_21()
, #eq^#(#0(), #pos(@y)) -> c_22()
, #eq^#(#s(@x), #0()) -> c_23()
, #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y))
, #eq^#(#neg(@x), #0()) -> c_25()
, #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y))
, #eq^#(#neg(@x), #pos(@y)) -> c_27()
, #eq^#(#pos(@x), #0()) -> c_28()
, #eq^#(#pos(@x), #neg(@y)) -> c_29()
, #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y))
, #mult^#(#0(), #0()) -> c_31()
, #mult^#(#0(), #neg(@y)) -> c_32()
, #mult^#(#0(), #pos(@y)) -> c_33()
, #mult^#(#neg(@x), #0()) -> c_34()
, #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_37()
, #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y))
, #sub^#(@x, #0()) -> c_40()
, #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y)))
, #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y)))
, #div^#(#0(), #0()) -> c_43()
, #div^#(#0(), #neg(@y)) -> c_44()
, #div^#(#0(), #pos(@y)) -> c_45()
, #div^#(#neg(@x), #0()) -> c_46()
, #div^#(#neg(@x), #neg(@y)) ->
c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#neg(@x), #pos(@y)) ->
c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #0()) -> c_49()
, #div^#(#pos(@x), #neg(@y)) ->
c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #pos(@y)) ->
c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #and^#(#false(), #false()) -> c_65()
, #and^#(#false(), #true()) -> c_66()
, #and^#(#true(), #false()) -> c_67()
, #and^#(#true(), #true()) -> c_68()
, #natmult^#(#0(), @y) -> c_85()
, #natmult^#(#s(@x), @y) ->
c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y))
, #add^#(#0(), @y) -> c_52()
, #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #positive^#(#0()) -> c_73()
, #positive^#(#s(@x)) -> c_74()
, #positive^#(#neg(@x)) -> c_75()
, #positive^#(#pos(@x)) -> c_76()
, #natdiv^#(#0(), #0()) -> c_69()
, #natdiv^#(#0(), #s(@y)) -> c_70()
, #natdiv^#(#s(@x), #0()) -> c_71()
, #natdiv^#(#s(@x), #s(@y)) ->
c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y))
, #negative^#(#0()) -> c_77()
, #negative^#(#s(@x)) -> c_78()
, #negative^#(#neg(@x)) -> c_79()
, #negative^#(#pos(@x)) -> c_80()
, #pred^#(#0()) -> c_57()
, #pred^#(#neg(#s(@x))) -> c_58()
, #pred^#(#pos(#s(#0()))) -> c_59()
, #pred^#(#pos(#s(#s(@x)))) -> c_60()
, #succ^#(#0()) -> c_61()
, #succ^#(#neg(#s(#0()))) -> c_62()
, #succ^#(#neg(#s(#s(@x)))) -> c_63()
, #succ^#(#pos(#s(@x))) -> c_64()
, #natdiv'^#(#0(), @y) -> c_89()
, #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y))
, #natdiv'^#(#underflow(), @y) -> c_91()
, #divsub^#(#0(), #0()) -> c_81()
, #divsub^#(#0(), #s(@y)) -> c_82()
, #divsub^#(#s(@x), #0()) -> c_83()
, #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y))
, #natadd^#(#0(), @y) -> c_87()
, #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y))
, #natsub^#(@x, #0()) -> c_92()
, #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, eratos(@l) -> eratos#1(@l)
, eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs)))
, eratos#1(nil()) -> nil()
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0()
, #natsub(@x, #0()) -> @x
, #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We estimate the number of application of {1,2,3,4,7,10,12,13} by
applications of Pre({1,2,3,4,7,10,12,13}) = {5,8,11,14}. Here rules
are labeled as follows:
DPs:
{ 1: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y))
, 2: *^#(@x, @y) -> c_2(#mult^#(@x, @y))
, 3: -^#(@x, @y) -> c_3(#sub^#(@x, @y))
, 4: div^#(@x, @y) -> c_4(#div^#(@x, @y))
, 5: eratos^#(@l) -> c_5(eratos#1^#(@l))
, 6: eratos#1^#(::(@x, @xs)) ->
c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, 7: eratos#1^#(nil()) -> c_7()
, 8: filter^#(@p, @l) -> c_8(filter#1^#(@l, @p))
, 9: filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs))
, 10: filter#1^#(nil(), @p) -> c_10()
, 11: filter#2^#(@xs', @p, @x) ->
c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'),
#equal^#(mod(@x, @p), #0()),
mod^#(@x, @p))
, 12: filter#3^#(#false(), @x, @xs') -> c_13()
, 13: filter#3^#(#true(), @x, @xs') -> c_14()
, 14: mod^#(@x, @y) ->
c_12(-^#(@x, *(@y, div(@x, @y))),
*^#(@y, div(@x, @y)),
div^#(@x, @y))
, 15: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, 16: #eq^#(::(@x_1, @x_2), nil()) -> c_16()
, 17: #eq^#(nil(), ::(@y_1, @y_2)) -> c_17()
, 18: #eq^#(nil(), nil()) -> c_18()
, 19: #eq^#(#0(), #0()) -> c_19()
, 20: #eq^#(#0(), #s(@y)) -> c_20()
, 21: #eq^#(#0(), #neg(@y)) -> c_21()
, 22: #eq^#(#0(), #pos(@y)) -> c_22()
, 23: #eq^#(#s(@x), #0()) -> c_23()
, 24: #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y))
, 25: #eq^#(#neg(@x), #0()) -> c_25()
, 26: #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y))
, 27: #eq^#(#neg(@x), #pos(@y)) -> c_27()
, 28: #eq^#(#pos(@x), #0()) -> c_28()
, 29: #eq^#(#pos(@x), #neg(@y)) -> c_29()
, 30: #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y))
, 31: #mult^#(#0(), #0()) -> c_31()
, 32: #mult^#(#0(), #neg(@y)) -> c_32()
, 33: #mult^#(#0(), #pos(@y)) -> c_33()
, 34: #mult^#(#neg(@x), #0()) -> c_34()
, 35: #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y))
, 36: #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y))
, 37: #mult^#(#pos(@x), #0()) -> c_37()
, 38: #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y))
, 39: #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y))
, 40: #sub^#(@x, #0()) -> c_40()
, 41: #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y)))
, 42: #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y)))
, 43: #div^#(#0(), #0()) -> c_43()
, 44: #div^#(#0(), #neg(@y)) -> c_44()
, 45: #div^#(#0(), #pos(@y)) -> c_45()
, 46: #div^#(#neg(@x), #0()) -> c_46()
, 47: #div^#(#neg(@x), #neg(@y)) ->
c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 48: #div^#(#neg(@x), #pos(@y)) ->
c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 49: #div^#(#pos(@x), #0()) -> c_49()
, 50: #div^#(#pos(@x), #neg(@y)) ->
c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 51: #div^#(#pos(@x), #pos(@y)) ->
c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 52: #and^#(#false(), #false()) -> c_65()
, 53: #and^#(#false(), #true()) -> c_66()
, 54: #and^#(#true(), #false()) -> c_67()
, 55: #and^#(#true(), #true()) -> c_68()
, 56: #natmult^#(#0(), @y) -> c_85()
, 57: #natmult^#(#s(@x), @y) ->
c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y))
, 58: #add^#(#0(), @y) -> c_52()
, 59: #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y))
, 60: #add^#(#neg(#s(#s(@x))), @y) ->
c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 61: #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y))
, 62: #add^#(#pos(#s(#s(@x))), @y) ->
c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 63: #positive^#(#0()) -> c_73()
, 64: #positive^#(#s(@x)) -> c_74()
, 65: #positive^#(#neg(@x)) -> c_75()
, 66: #positive^#(#pos(@x)) -> c_76()
, 67: #natdiv^#(#0(), #0()) -> c_69()
, 68: #natdiv^#(#0(), #s(@y)) -> c_70()
, 69: #natdiv^#(#s(@x), #0()) -> c_71()
, 70: #natdiv^#(#s(@x), #s(@y)) ->
c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y))
, 71: #negative^#(#0()) -> c_77()
, 72: #negative^#(#s(@x)) -> c_78()
, 73: #negative^#(#neg(@x)) -> c_79()
, 74: #negative^#(#pos(@x)) -> c_80()
, 75: #pred^#(#0()) -> c_57()
, 76: #pred^#(#neg(#s(@x))) -> c_58()
, 77: #pred^#(#pos(#s(#0()))) -> c_59()
, 78: #pred^#(#pos(#s(#s(@x)))) -> c_60()
, 79: #succ^#(#0()) -> c_61()
, 80: #succ^#(#neg(#s(#0()))) -> c_62()
, 81: #succ^#(#neg(#s(#s(@x)))) -> c_63()
, 82: #succ^#(#pos(#s(@x))) -> c_64()
, 83: #natdiv'^#(#0(), @y) -> c_89()
, 84: #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y))
, 85: #natdiv'^#(#underflow(), @y) -> c_91()
, 86: #divsub^#(#0(), #0()) -> c_81()
, 87: #divsub^#(#0(), #s(@y)) -> c_82()
, 88: #divsub^#(#s(@x), #0()) -> c_83()
, 89: #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y))
, 90: #natadd^#(#0(), @y) -> c_87()
, 91: #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y))
, 92: #natsub^#(@x, #0()) -> c_92()
, 93: #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eratos^#(@l) -> c_5(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, filter^#(@p, @l) -> c_8(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs))
, filter#2^#(@xs', @p, @x) ->
c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'),
#equal^#(mod(@x, @p), #0()),
mod^#(@x, @p))
, mod^#(@x, @y) ->
c_12(-^#(@x, *(@y, div(@x, @y))),
*^#(@y, div(@x, @y)),
div^#(@x, @y)) }
Weak DPs:
{ #equal^#(@x, @y) -> c_1(#eq^#(@x, @y))
, #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_16()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_17()
, #eq^#(nil(), nil()) -> c_18()
, #eq^#(#0(), #0()) -> c_19()
, #eq^#(#0(), #s(@y)) -> c_20()
, #eq^#(#0(), #neg(@y)) -> c_21()
, #eq^#(#0(), #pos(@y)) -> c_22()
, #eq^#(#s(@x), #0()) -> c_23()
, #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y))
, #eq^#(#neg(@x), #0()) -> c_25()
, #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y))
, #eq^#(#neg(@x), #pos(@y)) -> c_27()
, #eq^#(#pos(@x), #0()) -> c_28()
, #eq^#(#pos(@x), #neg(@y)) -> c_29()
, #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y))
, *^#(@x, @y) -> c_2(#mult^#(@x, @y))
, #mult^#(#0(), #0()) -> c_31()
, #mult^#(#0(), #neg(@y)) -> c_32()
, #mult^#(#0(), #pos(@y)) -> c_33()
, #mult^#(#neg(@x), #0()) -> c_34()
, #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_37()
, #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y))
, -^#(@x, @y) -> c_3(#sub^#(@x, @y))
, #sub^#(@x, #0()) -> c_40()
, #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y)))
, #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y)))
, div^#(@x, @y) -> c_4(#div^#(@x, @y))
, #div^#(#0(), #0()) -> c_43()
, #div^#(#0(), #neg(@y)) -> c_44()
, #div^#(#0(), #pos(@y)) -> c_45()
, #div^#(#neg(@x), #0()) -> c_46()
, #div^#(#neg(@x), #neg(@y)) ->
c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#neg(@x), #pos(@y)) ->
c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #0()) -> c_49()
, #div^#(#pos(@x), #neg(@y)) ->
c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #pos(@y)) ->
c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, eratos#1^#(nil()) -> c_7()
, filter#1^#(nil(), @p) -> c_10()
, filter#3^#(#false(), @x, @xs') -> c_13()
, filter#3^#(#true(), @x, @xs') -> c_14()
, #and^#(#false(), #false()) -> c_65()
, #and^#(#false(), #true()) -> c_66()
, #and^#(#true(), #false()) -> c_67()
, #and^#(#true(), #true()) -> c_68()
, #natmult^#(#0(), @y) -> c_85()
, #natmult^#(#s(@x), @y) ->
c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y))
, #add^#(#0(), @y) -> c_52()
, #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #positive^#(#0()) -> c_73()
, #positive^#(#s(@x)) -> c_74()
, #positive^#(#neg(@x)) -> c_75()
, #positive^#(#pos(@x)) -> c_76()
, #natdiv^#(#0(), #0()) -> c_69()
, #natdiv^#(#0(), #s(@y)) -> c_70()
, #natdiv^#(#s(@x), #0()) -> c_71()
, #natdiv^#(#s(@x), #s(@y)) ->
c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y))
, #negative^#(#0()) -> c_77()
, #negative^#(#s(@x)) -> c_78()
, #negative^#(#neg(@x)) -> c_79()
, #negative^#(#pos(@x)) -> c_80()
, #pred^#(#0()) -> c_57()
, #pred^#(#neg(#s(@x))) -> c_58()
, #pred^#(#pos(#s(#0()))) -> c_59()
, #pred^#(#pos(#s(#s(@x)))) -> c_60()
, #succ^#(#0()) -> c_61()
, #succ^#(#neg(#s(#0()))) -> c_62()
, #succ^#(#neg(#s(#s(@x)))) -> c_63()
, #succ^#(#pos(#s(@x))) -> c_64()
, #natdiv'^#(#0(), @y) -> c_89()
, #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y))
, #natdiv'^#(#underflow(), @y) -> c_91()
, #divsub^#(#0(), #0()) -> c_81()
, #divsub^#(#0(), #s(@y)) -> c_82()
, #divsub^#(#s(@x), #0()) -> c_83()
, #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y))
, #natadd^#(#0(), @y) -> c_87()
, #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y))
, #natsub^#(@x, #0()) -> c_92()
, #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, eratos(@l) -> eratos#1(@l)
, eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs)))
, eratos#1(nil()) -> nil()
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0()
, #natsub(@x, #0()) -> @x
, #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We estimate the number of application of {6} by applications of
Pre({6}) = {5}. Here rules are labeled as follows:
DPs:
{ 1: eratos^#(@l) -> c_5(eratos#1^#(@l))
, 2: eratos#1^#(::(@x, @xs)) ->
c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, 3: filter^#(@p, @l) -> c_8(filter#1^#(@l, @p))
, 4: filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs))
, 5: filter#2^#(@xs', @p, @x) ->
c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'),
#equal^#(mod(@x, @p), #0()),
mod^#(@x, @p))
, 6: mod^#(@x, @y) ->
c_12(-^#(@x, *(@y, div(@x, @y))),
*^#(@y, div(@x, @y)),
div^#(@x, @y))
, 7: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y))
, 8: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, 9: #eq^#(::(@x_1, @x_2), nil()) -> c_16()
, 10: #eq^#(nil(), ::(@y_1, @y_2)) -> c_17()
, 11: #eq^#(nil(), nil()) -> c_18()
, 12: #eq^#(#0(), #0()) -> c_19()
, 13: #eq^#(#0(), #s(@y)) -> c_20()
, 14: #eq^#(#0(), #neg(@y)) -> c_21()
, 15: #eq^#(#0(), #pos(@y)) -> c_22()
, 16: #eq^#(#s(@x), #0()) -> c_23()
, 17: #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y))
, 18: #eq^#(#neg(@x), #0()) -> c_25()
, 19: #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y))
, 20: #eq^#(#neg(@x), #pos(@y)) -> c_27()
, 21: #eq^#(#pos(@x), #0()) -> c_28()
, 22: #eq^#(#pos(@x), #neg(@y)) -> c_29()
, 23: #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y))
, 24: *^#(@x, @y) -> c_2(#mult^#(@x, @y))
, 25: #mult^#(#0(), #0()) -> c_31()
, 26: #mult^#(#0(), #neg(@y)) -> c_32()
, 27: #mult^#(#0(), #pos(@y)) -> c_33()
, 28: #mult^#(#neg(@x), #0()) -> c_34()
, 29: #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y))
, 30: #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y))
, 31: #mult^#(#pos(@x), #0()) -> c_37()
, 32: #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y))
, 33: #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y))
, 34: -^#(@x, @y) -> c_3(#sub^#(@x, @y))
, 35: #sub^#(@x, #0()) -> c_40()
, 36: #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y)))
, 37: #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y)))
, 38: div^#(@x, @y) -> c_4(#div^#(@x, @y))
, 39: #div^#(#0(), #0()) -> c_43()
, 40: #div^#(#0(), #neg(@y)) -> c_44()
, 41: #div^#(#0(), #pos(@y)) -> c_45()
, 42: #div^#(#neg(@x), #0()) -> c_46()
, 43: #div^#(#neg(@x), #neg(@y)) ->
c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 44: #div^#(#neg(@x), #pos(@y)) ->
c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 45: #div^#(#pos(@x), #0()) -> c_49()
, 46: #div^#(#pos(@x), #neg(@y)) ->
c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 47: #div^#(#pos(@x), #pos(@y)) ->
c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 48: eratos#1^#(nil()) -> c_7()
, 49: filter#1^#(nil(), @p) -> c_10()
, 50: filter#3^#(#false(), @x, @xs') -> c_13()
, 51: filter#3^#(#true(), @x, @xs') -> c_14()
, 52: #and^#(#false(), #false()) -> c_65()
, 53: #and^#(#false(), #true()) -> c_66()
, 54: #and^#(#true(), #false()) -> c_67()
, 55: #and^#(#true(), #true()) -> c_68()
, 56: #natmult^#(#0(), @y) -> c_85()
, 57: #natmult^#(#s(@x), @y) ->
c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y))
, 58: #add^#(#0(), @y) -> c_52()
, 59: #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y))
, 60: #add^#(#neg(#s(#s(@x))), @y) ->
c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 61: #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y))
, 62: #add^#(#pos(#s(#s(@x))), @y) ->
c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 63: #positive^#(#0()) -> c_73()
, 64: #positive^#(#s(@x)) -> c_74()
, 65: #positive^#(#neg(@x)) -> c_75()
, 66: #positive^#(#pos(@x)) -> c_76()
, 67: #natdiv^#(#0(), #0()) -> c_69()
, 68: #natdiv^#(#0(), #s(@y)) -> c_70()
, 69: #natdiv^#(#s(@x), #0()) -> c_71()
, 70: #natdiv^#(#s(@x), #s(@y)) ->
c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y))
, 71: #negative^#(#0()) -> c_77()
, 72: #negative^#(#s(@x)) -> c_78()
, 73: #negative^#(#neg(@x)) -> c_79()
, 74: #negative^#(#pos(@x)) -> c_80()
, 75: #pred^#(#0()) -> c_57()
, 76: #pred^#(#neg(#s(@x))) -> c_58()
, 77: #pred^#(#pos(#s(#0()))) -> c_59()
, 78: #pred^#(#pos(#s(#s(@x)))) -> c_60()
, 79: #succ^#(#0()) -> c_61()
, 80: #succ^#(#neg(#s(#0()))) -> c_62()
, 81: #succ^#(#neg(#s(#s(@x)))) -> c_63()
, 82: #succ^#(#pos(#s(@x))) -> c_64()
, 83: #natdiv'^#(#0(), @y) -> c_89()
, 84: #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y))
, 85: #natdiv'^#(#underflow(), @y) -> c_91()
, 86: #divsub^#(#0(), #0()) -> c_81()
, 87: #divsub^#(#0(), #s(@y)) -> c_82()
, 88: #divsub^#(#s(@x), #0()) -> c_83()
, 89: #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y))
, 90: #natadd^#(#0(), @y) -> c_87()
, 91: #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y))
, 92: #natsub^#(@x, #0()) -> c_92()
, 93: #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eratos^#(@l) -> c_5(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, filter^#(@p, @l) -> c_8(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs))
, filter#2^#(@xs', @p, @x) ->
c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'),
#equal^#(mod(@x, @p), #0()),
mod^#(@x, @p)) }
Weak DPs:
{ #equal^#(@x, @y) -> c_1(#eq^#(@x, @y))
, #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_16()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_17()
, #eq^#(nil(), nil()) -> c_18()
, #eq^#(#0(), #0()) -> c_19()
, #eq^#(#0(), #s(@y)) -> c_20()
, #eq^#(#0(), #neg(@y)) -> c_21()
, #eq^#(#0(), #pos(@y)) -> c_22()
, #eq^#(#s(@x), #0()) -> c_23()
, #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y))
, #eq^#(#neg(@x), #0()) -> c_25()
, #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y))
, #eq^#(#neg(@x), #pos(@y)) -> c_27()
, #eq^#(#pos(@x), #0()) -> c_28()
, #eq^#(#pos(@x), #neg(@y)) -> c_29()
, #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y))
, *^#(@x, @y) -> c_2(#mult^#(@x, @y))
, #mult^#(#0(), #0()) -> c_31()
, #mult^#(#0(), #neg(@y)) -> c_32()
, #mult^#(#0(), #pos(@y)) -> c_33()
, #mult^#(#neg(@x), #0()) -> c_34()
, #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_37()
, #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y))
, -^#(@x, @y) -> c_3(#sub^#(@x, @y))
, #sub^#(@x, #0()) -> c_40()
, #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y)))
, #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y)))
, div^#(@x, @y) -> c_4(#div^#(@x, @y))
, #div^#(#0(), #0()) -> c_43()
, #div^#(#0(), #neg(@y)) -> c_44()
, #div^#(#0(), #pos(@y)) -> c_45()
, #div^#(#neg(@x), #0()) -> c_46()
, #div^#(#neg(@x), #neg(@y)) ->
c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#neg(@x), #pos(@y)) ->
c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #0()) -> c_49()
, #div^#(#pos(@x), #neg(@y)) ->
c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #pos(@y)) ->
c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, eratos#1^#(nil()) -> c_7()
, filter#1^#(nil(), @p) -> c_10()
, filter#3^#(#false(), @x, @xs') -> c_13()
, filter#3^#(#true(), @x, @xs') -> c_14()
, mod^#(@x, @y) ->
c_12(-^#(@x, *(@y, div(@x, @y))),
*^#(@y, div(@x, @y)),
div^#(@x, @y))
, #and^#(#false(), #false()) -> c_65()
, #and^#(#false(), #true()) -> c_66()
, #and^#(#true(), #false()) -> c_67()
, #and^#(#true(), #true()) -> c_68()
, #natmult^#(#0(), @y) -> c_85()
, #natmult^#(#s(@x), @y) ->
c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y))
, #add^#(#0(), @y) -> c_52()
, #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #positive^#(#0()) -> c_73()
, #positive^#(#s(@x)) -> c_74()
, #positive^#(#neg(@x)) -> c_75()
, #positive^#(#pos(@x)) -> c_76()
, #natdiv^#(#0(), #0()) -> c_69()
, #natdiv^#(#0(), #s(@y)) -> c_70()
, #natdiv^#(#s(@x), #0()) -> c_71()
, #natdiv^#(#s(@x), #s(@y)) ->
c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y))
, #negative^#(#0()) -> c_77()
, #negative^#(#s(@x)) -> c_78()
, #negative^#(#neg(@x)) -> c_79()
, #negative^#(#pos(@x)) -> c_80()
, #pred^#(#0()) -> c_57()
, #pred^#(#neg(#s(@x))) -> c_58()
, #pred^#(#pos(#s(#0()))) -> c_59()
, #pred^#(#pos(#s(#s(@x)))) -> c_60()
, #succ^#(#0()) -> c_61()
, #succ^#(#neg(#s(#0()))) -> c_62()
, #succ^#(#neg(#s(#s(@x)))) -> c_63()
, #succ^#(#pos(#s(@x))) -> c_64()
, #natdiv'^#(#0(), @y) -> c_89()
, #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y))
, #natdiv'^#(#underflow(), @y) -> c_91()
, #divsub^#(#0(), #0()) -> c_81()
, #divsub^#(#0(), #s(@y)) -> c_82()
, #divsub^#(#s(@x), #0()) -> c_83()
, #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y))
, #natadd^#(#0(), @y) -> c_87()
, #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y))
, #natsub^#(@x, #0()) -> c_92()
, #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, eratos(@l) -> eratos#1(@l)
, eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs)))
, eratos#1(nil()) -> nil()
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0()
, #natsub(@x, #0()) -> @x
, #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We estimate the number of application of {5} by applications of
Pre({5}) = {4}. Here rules are labeled as follows:
DPs:
{ 1: eratos^#(@l) -> c_5(eratos#1^#(@l))
, 2: eratos#1^#(::(@x, @xs)) ->
c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, 3: filter^#(@p, @l) -> c_8(filter#1^#(@l, @p))
, 4: filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs))
, 5: filter#2^#(@xs', @p, @x) ->
c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'),
#equal^#(mod(@x, @p), #0()),
mod^#(@x, @p))
, 6: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y))
, 7: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, 8: #eq^#(::(@x_1, @x_2), nil()) -> c_16()
, 9: #eq^#(nil(), ::(@y_1, @y_2)) -> c_17()
, 10: #eq^#(nil(), nil()) -> c_18()
, 11: #eq^#(#0(), #0()) -> c_19()
, 12: #eq^#(#0(), #s(@y)) -> c_20()
, 13: #eq^#(#0(), #neg(@y)) -> c_21()
, 14: #eq^#(#0(), #pos(@y)) -> c_22()
, 15: #eq^#(#s(@x), #0()) -> c_23()
, 16: #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y))
, 17: #eq^#(#neg(@x), #0()) -> c_25()
, 18: #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y))
, 19: #eq^#(#neg(@x), #pos(@y)) -> c_27()
, 20: #eq^#(#pos(@x), #0()) -> c_28()
, 21: #eq^#(#pos(@x), #neg(@y)) -> c_29()
, 22: #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y))
, 23: *^#(@x, @y) -> c_2(#mult^#(@x, @y))
, 24: #mult^#(#0(), #0()) -> c_31()
, 25: #mult^#(#0(), #neg(@y)) -> c_32()
, 26: #mult^#(#0(), #pos(@y)) -> c_33()
, 27: #mult^#(#neg(@x), #0()) -> c_34()
, 28: #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y))
, 29: #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y))
, 30: #mult^#(#pos(@x), #0()) -> c_37()
, 31: #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y))
, 32: #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y))
, 33: -^#(@x, @y) -> c_3(#sub^#(@x, @y))
, 34: #sub^#(@x, #0()) -> c_40()
, 35: #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y)))
, 36: #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y)))
, 37: div^#(@x, @y) -> c_4(#div^#(@x, @y))
, 38: #div^#(#0(), #0()) -> c_43()
, 39: #div^#(#0(), #neg(@y)) -> c_44()
, 40: #div^#(#0(), #pos(@y)) -> c_45()
, 41: #div^#(#neg(@x), #0()) -> c_46()
, 42: #div^#(#neg(@x), #neg(@y)) ->
c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 43: #div^#(#neg(@x), #pos(@y)) ->
c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 44: #div^#(#pos(@x), #0()) -> c_49()
, 45: #div^#(#pos(@x), #neg(@y)) ->
c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 46: #div^#(#pos(@x), #pos(@y)) ->
c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, 47: eratos#1^#(nil()) -> c_7()
, 48: filter#1^#(nil(), @p) -> c_10()
, 49: filter#3^#(#false(), @x, @xs') -> c_13()
, 50: filter#3^#(#true(), @x, @xs') -> c_14()
, 51: mod^#(@x, @y) ->
c_12(-^#(@x, *(@y, div(@x, @y))),
*^#(@y, div(@x, @y)),
div^#(@x, @y))
, 52: #and^#(#false(), #false()) -> c_65()
, 53: #and^#(#false(), #true()) -> c_66()
, 54: #and^#(#true(), #false()) -> c_67()
, 55: #and^#(#true(), #true()) -> c_68()
, 56: #natmult^#(#0(), @y) -> c_85()
, 57: #natmult^#(#s(@x), @y) ->
c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y))
, 58: #add^#(#0(), @y) -> c_52()
, 59: #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y))
, 60: #add^#(#neg(#s(#s(@x))), @y) ->
c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 61: #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y))
, 62: #add^#(#pos(#s(#s(@x))), @y) ->
c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 63: #positive^#(#0()) -> c_73()
, 64: #positive^#(#s(@x)) -> c_74()
, 65: #positive^#(#neg(@x)) -> c_75()
, 66: #positive^#(#pos(@x)) -> c_76()
, 67: #natdiv^#(#0(), #0()) -> c_69()
, 68: #natdiv^#(#0(), #s(@y)) -> c_70()
, 69: #natdiv^#(#s(@x), #0()) -> c_71()
, 70: #natdiv^#(#s(@x), #s(@y)) ->
c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y))
, 71: #negative^#(#0()) -> c_77()
, 72: #negative^#(#s(@x)) -> c_78()
, 73: #negative^#(#neg(@x)) -> c_79()
, 74: #negative^#(#pos(@x)) -> c_80()
, 75: #pred^#(#0()) -> c_57()
, 76: #pred^#(#neg(#s(@x))) -> c_58()
, 77: #pred^#(#pos(#s(#0()))) -> c_59()
, 78: #pred^#(#pos(#s(#s(@x)))) -> c_60()
, 79: #succ^#(#0()) -> c_61()
, 80: #succ^#(#neg(#s(#0()))) -> c_62()
, 81: #succ^#(#neg(#s(#s(@x)))) -> c_63()
, 82: #succ^#(#pos(#s(@x))) -> c_64()
, 83: #natdiv'^#(#0(), @y) -> c_89()
, 84: #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y))
, 85: #natdiv'^#(#underflow(), @y) -> c_91()
, 86: #divsub^#(#0(), #0()) -> c_81()
, 87: #divsub^#(#0(), #s(@y)) -> c_82()
, 88: #divsub^#(#s(@x), #0()) -> c_83()
, 89: #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y))
, 90: #natadd^#(#0(), @y) -> c_87()
, 91: #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y))
, 92: #natsub^#(@x, #0()) -> c_92()
, 93: #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eratos^#(@l) -> c_5(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, filter^#(@p, @l) -> c_8(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) }
Weak DPs:
{ #equal^#(@x, @y) -> c_1(#eq^#(@x, @y))
, #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_16()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_17()
, #eq^#(nil(), nil()) -> c_18()
, #eq^#(#0(), #0()) -> c_19()
, #eq^#(#0(), #s(@y)) -> c_20()
, #eq^#(#0(), #neg(@y)) -> c_21()
, #eq^#(#0(), #pos(@y)) -> c_22()
, #eq^#(#s(@x), #0()) -> c_23()
, #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y))
, #eq^#(#neg(@x), #0()) -> c_25()
, #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y))
, #eq^#(#neg(@x), #pos(@y)) -> c_27()
, #eq^#(#pos(@x), #0()) -> c_28()
, #eq^#(#pos(@x), #neg(@y)) -> c_29()
, #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y))
, *^#(@x, @y) -> c_2(#mult^#(@x, @y))
, #mult^#(#0(), #0()) -> c_31()
, #mult^#(#0(), #neg(@y)) -> c_32()
, #mult^#(#0(), #pos(@y)) -> c_33()
, #mult^#(#neg(@x), #0()) -> c_34()
, #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_37()
, #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y))
, -^#(@x, @y) -> c_3(#sub^#(@x, @y))
, #sub^#(@x, #0()) -> c_40()
, #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y)))
, #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y)))
, div^#(@x, @y) -> c_4(#div^#(@x, @y))
, #div^#(#0(), #0()) -> c_43()
, #div^#(#0(), #neg(@y)) -> c_44()
, #div^#(#0(), #pos(@y)) -> c_45()
, #div^#(#neg(@x), #0()) -> c_46()
, #div^#(#neg(@x), #neg(@y)) ->
c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#neg(@x), #pos(@y)) ->
c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #0()) -> c_49()
, #div^#(#pos(@x), #neg(@y)) ->
c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #pos(@y)) ->
c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, eratos#1^#(nil()) -> c_7()
, filter#1^#(nil(), @p) -> c_10()
, filter#2^#(@xs', @p, @x) ->
c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'),
#equal^#(mod(@x, @p), #0()),
mod^#(@x, @p))
, filter#3^#(#false(), @x, @xs') -> c_13()
, filter#3^#(#true(), @x, @xs') -> c_14()
, mod^#(@x, @y) ->
c_12(-^#(@x, *(@y, div(@x, @y))),
*^#(@y, div(@x, @y)),
div^#(@x, @y))
, #and^#(#false(), #false()) -> c_65()
, #and^#(#false(), #true()) -> c_66()
, #and^#(#true(), #false()) -> c_67()
, #and^#(#true(), #true()) -> c_68()
, #natmult^#(#0(), @y) -> c_85()
, #natmult^#(#s(@x), @y) ->
c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y))
, #add^#(#0(), @y) -> c_52()
, #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #positive^#(#0()) -> c_73()
, #positive^#(#s(@x)) -> c_74()
, #positive^#(#neg(@x)) -> c_75()
, #positive^#(#pos(@x)) -> c_76()
, #natdiv^#(#0(), #0()) -> c_69()
, #natdiv^#(#0(), #s(@y)) -> c_70()
, #natdiv^#(#s(@x), #0()) -> c_71()
, #natdiv^#(#s(@x), #s(@y)) ->
c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y))
, #negative^#(#0()) -> c_77()
, #negative^#(#s(@x)) -> c_78()
, #negative^#(#neg(@x)) -> c_79()
, #negative^#(#pos(@x)) -> c_80()
, #pred^#(#0()) -> c_57()
, #pred^#(#neg(#s(@x))) -> c_58()
, #pred^#(#pos(#s(#0()))) -> c_59()
, #pred^#(#pos(#s(#s(@x)))) -> c_60()
, #succ^#(#0()) -> c_61()
, #succ^#(#neg(#s(#0()))) -> c_62()
, #succ^#(#neg(#s(#s(@x)))) -> c_63()
, #succ^#(#pos(#s(@x))) -> c_64()
, #natdiv'^#(#0(), @y) -> c_89()
, #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y))
, #natdiv'^#(#underflow(), @y) -> c_91()
, #divsub^#(#0(), #0()) -> c_81()
, #divsub^#(#0(), #s(@y)) -> c_82()
, #divsub^#(#s(@x), #0()) -> c_83()
, #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y))
, #natadd^#(#0(), @y) -> c_87()
, #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y))
, #natsub^#(@x, #0()) -> c_92()
, #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, eratos(@l) -> eratos#1(@l)
, eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs)))
, eratos#1(nil()) -> nil()
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0()
, #natsub(@x, #0()) -> @x
, #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ #equal^#(@x, @y) -> c_1(#eq^#(@x, @y))
, #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)),
#eq^#(@x_1, @y_1),
#eq^#(@x_2, @y_2))
, #eq^#(::(@x_1, @x_2), nil()) -> c_16()
, #eq^#(nil(), ::(@y_1, @y_2)) -> c_17()
, #eq^#(nil(), nil()) -> c_18()
, #eq^#(#0(), #0()) -> c_19()
, #eq^#(#0(), #s(@y)) -> c_20()
, #eq^#(#0(), #neg(@y)) -> c_21()
, #eq^#(#0(), #pos(@y)) -> c_22()
, #eq^#(#s(@x), #0()) -> c_23()
, #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y))
, #eq^#(#neg(@x), #0()) -> c_25()
, #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y))
, #eq^#(#neg(@x), #pos(@y)) -> c_27()
, #eq^#(#pos(@x), #0()) -> c_28()
, #eq^#(#pos(@x), #neg(@y)) -> c_29()
, #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y))
, *^#(@x, @y) -> c_2(#mult^#(@x, @y))
, #mult^#(#0(), #0()) -> c_31()
, #mult^#(#0(), #neg(@y)) -> c_32()
, #mult^#(#0(), #pos(@y)) -> c_33()
, #mult^#(#neg(@x), #0()) -> c_34()
, #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_37()
, #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y))
, -^#(@x, @y) -> c_3(#sub^#(@x, @y))
, #sub^#(@x, #0()) -> c_40()
, #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y)))
, #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y)))
, div^#(@x, @y) -> c_4(#div^#(@x, @y))
, #div^#(#0(), #0()) -> c_43()
, #div^#(#0(), #neg(@y)) -> c_44()
, #div^#(#0(), #pos(@y)) -> c_45()
, #div^#(#neg(@x), #0()) -> c_46()
, #div^#(#neg(@x), #neg(@y)) ->
c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#neg(@x), #pos(@y)) ->
c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #0()) -> c_49()
, #div^#(#pos(@x), #neg(@y)) ->
c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, #div^#(#pos(@x), #pos(@y)) ->
c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y))
, eratos#1^#(nil()) -> c_7()
, filter#1^#(nil(), @p) -> c_10()
, filter#2^#(@xs', @p, @x) ->
c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'),
#equal^#(mod(@x, @p), #0()),
mod^#(@x, @p))
, filter#3^#(#false(), @x, @xs') -> c_13()
, filter#3^#(#true(), @x, @xs') -> c_14()
, mod^#(@x, @y) ->
c_12(-^#(@x, *(@y, div(@x, @y))),
*^#(@y, div(@x, @y)),
div^#(@x, @y))
, #and^#(#false(), #false()) -> c_65()
, #and^#(#false(), #true()) -> c_66()
, #and^#(#true(), #false()) -> c_67()
, #and^#(#true(), #true()) -> c_68()
, #natmult^#(#0(), @y) -> c_85()
, #natmult^#(#s(@x), @y) ->
c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y))
, #add^#(#0(), @y) -> c_52()
, #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #positive^#(#0()) -> c_73()
, #positive^#(#s(@x)) -> c_74()
, #positive^#(#neg(@x)) -> c_75()
, #positive^#(#pos(@x)) -> c_76()
, #natdiv^#(#0(), #0()) -> c_69()
, #natdiv^#(#0(), #s(@y)) -> c_70()
, #natdiv^#(#s(@x), #0()) -> c_71()
, #natdiv^#(#s(@x), #s(@y)) ->
c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y))
, #negative^#(#0()) -> c_77()
, #negative^#(#s(@x)) -> c_78()
, #negative^#(#neg(@x)) -> c_79()
, #negative^#(#pos(@x)) -> c_80()
, #pred^#(#0()) -> c_57()
, #pred^#(#neg(#s(@x))) -> c_58()
, #pred^#(#pos(#s(#0()))) -> c_59()
, #pred^#(#pos(#s(#s(@x)))) -> c_60()
, #succ^#(#0()) -> c_61()
, #succ^#(#neg(#s(#0()))) -> c_62()
, #succ^#(#neg(#s(#s(@x)))) -> c_63()
, #succ^#(#pos(#s(@x))) -> c_64()
, #natdiv'^#(#0(), @y) -> c_89()
, #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y))
, #natdiv'^#(#underflow(), @y) -> c_91()
, #divsub^#(#0(), #0()) -> c_81()
, #divsub^#(#0(), #s(@y)) -> c_82()
, #divsub^#(#s(@x), #0()) -> c_83()
, #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y))
, #natadd^#(#0(), @y) -> c_87()
, #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y))
, #natsub^#(@x, #0()) -> c_92()
, #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eratos^#(@l) -> c_5(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, filter^#(@p, @l) -> c_8(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, eratos(@l) -> eratos#1(@l)
, eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs)))
, eratos#1(nil()) -> nil()
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0()
, #natsub(@x, #0()) -> @x
, #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ filter#1^#(::(@x, @xs), @p) ->
c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eratos^#(@l) -> c_1(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, filter^#(@p, @l) -> c_3(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, eratos(@l) -> eratos#1(@l)
, eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs)))
, eratos#1(nil()) -> nil()
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0()
, #natsub(@x, #0()) -> @x
, #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eratos^#(@l) -> c_1(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, filter^#(@p, @l) -> c_3(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 4: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) }
Trs:
{ #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #sub(@x, #0()) -> @x
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, #add(#0(), @y) -> @y
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natdiv'(#0(), @y) -> #s(#0()) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
Uargs(c_4) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#equal](x1, x2) = [0 0] x1 + [0 2] x2 + [1]
[0 2] [0 0] [0]
[#eq](x1, x2) = [1]
[0]
[*](x1, x2) = [2 0] x1 + [2 0] x2 + [0]
[0 0] [2 0] [1]
[#mult](x1, x2) = [1 0] x2 + [0]
[0 0] [1]
[-](x1, x2) = [1 0] x1 + [2]
[2 1] [2]
[#sub](x1, x2) = [1 0] x1 + [2]
[2 1] [2]
[div](x1, x2) = [2 0] x1 + [1 0] x2 + [0]
[2 2] [1 0] [0]
[#div](x1, x2) = [2 0] x1 + [0]
[2 2] [0]
[eratos](x1) = [0]
[0]
[eratos#1](x1) = [0]
[0]
[::](x1, x2) = [1 0] x1 + [1 2] x2 + [0]
[0 0] [0 1] [1]
[filter](x1, x2) = [1 1] x2 + [0]
[0 1] [0]
[nil] = [0]
[0]
[filter#1](x1, x2) = [1 1] x1 + [0]
[0 1] [0]
[filter#2](x1, x2, x3) = [1 2] x1 + [1 0] x3 + [0]
[0 1] [0 0] [1]
[mod](x1, x2) = [1 0] x1 + [2]
[2 1] [2]
[#0] = [2]
[0]
[filter#3](x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 2] x3 + [0]
[1 0] [0 0] [0 1] [0]
[#false] = [1]
[0]
[#true] = [0]
[0]
[#add](x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[2 1] [2 1] [0]
[#s](x1) = [1 0] x1 + [2]
[0 0] [1]
[#neg](x1) = [1]
[0]
[#pred](x1) = [2]
[2]
[#pos](x1) = [1]
[0]
[#succ](x1) = [0 0] x1 + [2]
[1 0] [0]
[#and](x1, x2) = [1]
[0]
[#divByZero] = [0]
[0]
[#natdiv](x1, x2) = [2 0] x1 + [0 0] x2 + [0]
[0 0] [0 2] [2]
[#positive](x1) = [2 0] x1 + [2]
[0 0] [0]
[#negative](x1) = [1]
[0]
[#divsub](x1, x2) = [1 0] x1 + [0 0] x2 + [1]
[0 0] [1 0] [1]
[#underflow] = [0]
[0]
[#natmult](x1, x2) = [2]
[1]
[#natadd](x1, x2) = [2 1] x1 + [2 1] x2 + [1]
[0 0] [0 0] [1]
[#natdiv'](x1, x2) = [2 0] x1 + [0 0] x2 + [2]
[0 0] [0 2] [2]
[#natsub](x1, x2) = [0]
[0]
[#equal^#](x1, x2) = [0]
[0]
[c_1](x1) = [0]
[0]
[#eq^#](x1, x2) = [0]
[0]
[*^#](x1, x2) = [0]
[0]
[c_2](x1) = [0]
[0]
[#mult^#](x1, x2) = [0]
[0]
[-^#](x1, x2) = [0]
[0]
[c_3](x1) = [0]
[0]
[#sub^#](x1, x2) = [0]
[0]
[div^#](x1, x2) = [0]
[0]
[c_4](x1) = [0]
[0]
[#div^#](x1, x2) = [0]
[0]
[eratos^#](x1) = [2 0] x1 + [1]
[1 1] [0]
[c_5](x1) = [0]
[0]
[eratos#1^#](x1) = [2 0] x1 + [1]
[0 0] [0]
[c_6](x1, x2) = [0]
[0]
[filter^#](x1, x2) = [0 2] x2 + [0]
[1 0] [2]
[c_7] = [0]
[0]
[c_8](x1) = [0]
[0]
[filter#1^#](x1, x2) = [0 2] x1 + [0]
[0 0] [0]
[c_9](x1, x2) = [0]
[0]
[filter#2^#](x1, x2, x3) = [0]
[0]
[c_10] = [0]
[0]
[c_11](x1, x2, x3) = [0]
[0]
[filter#3^#](x1, x2, x3) = [0]
[0]
[mod^#](x1, x2) = [0]
[0]
[c_12](x1, x2, x3) = [0]
[0]
[c_13] = [0]
[0]
[c_14] = [0]
[0]
[c_15](x1, x2, x3) = [0]
[0]
[#and^#](x1, x2) = [0]
[0]
[c_16] = [0]
[0]
[c_17] = [0]
[0]
[c_18] = [0]
[0]
[c_19] = [0]
[0]
[c_20] = [0]
[0]
[c_21] = [0]
[0]
[c_22] = [0]
[0]
[c_23] = [0]
[0]
[c_24](x1) = [0]
[0]
[c_25] = [0]
[0]
[c_26](x1) = [0]
[0]
[c_27] = [0]
[0]
[c_28] = [0]
[0]
[c_29] = [0]
[0]
[c_30](x1) = [0]
[0]
[c_31] = [0]
[0]
[c_32] = [0]
[0]
[c_33] = [0]
[0]
[c_34] = [0]
[0]
[c_35](x1) = [0]
[0]
[#natmult^#](x1, x2) = [0]
[0]
[c_36](x1) = [0]
[0]
[c_37] = [0]
[0]
[c_38](x1) = [0]
[0]
[c_39](x1) = [0]
[0]
[c_40] = [0]
[0]
[c_41](x1) = [0]
[0]
[#add^#](x1, x2) = [0]
[0]
[c_42](x1) = [0]
[0]
[c_43] = [0]
[0]
[c_44] = [0]
[0]
[c_45] = [0]
[0]
[c_46] = [0]
[0]
[c_47](x1, x2) = [0]
[0]
[#positive^#](x1) = [0]
[0]
[#natdiv^#](x1, x2) = [0]
[0]
[c_48](x1, x2) = [0]
[0]
[#negative^#](x1) = [0]
[0]
[c_49] = [0]
[0]
[c_50](x1, x2) = [0]
[0]
[c_51](x1, x2) = [0]
[0]
[c_52] = [0]
[0]
[c_53](x1) = [0]
[0]
[#pred^#](x1) = [0]
[0]
[c_54](x1, x2) = [0]
[0]
[c_55](x1) = [0]
[0]
[#succ^#](x1) = [0]
[0]
[c_56](x1, x2) = [0]
[0]
[c_57] = [0]
[0]
[c_58] = [0]
[0]
[c_59] = [0]
[0]
[c_60] = [0]
[0]
[c_61] = [0]
[0]
[c_62] = [0]
[0]
[c_63] = [0]
[0]
[c_64] = [0]
[0]
[c_65] = [0]
[0]
[c_66] = [0]
[0]
[c_67] = [0]
[0]
[c_68] = [0]
[0]
[c_69] = [0]
[0]
[c_70] = [0]
[0]
[c_71] = [0]
[0]
[c_72](x1, x2) = [0]
[0]
[#natdiv'^#](x1, x2) = [0]
[0]
[#divsub^#](x1, x2) = [0]
[0]
[c_73] = [0]
[0]
[c_74] = [0]
[0]
[c_75] = [0]
[0]
[c_76] = [0]
[0]
[c_77] = [0]
[0]
[c_78] = [0]
[0]
[c_79] = [0]
[0]
[c_80] = [0]
[0]
[c_81] = [0]
[0]
[c_82] = [0]
[0]
[c_83] = [0]
[0]
[c_84](x1) = [0]
[0]
[c_85] = [0]
[0]
[c_86](x1, x2) = [0]
[0]
[#natadd^#](x1, x2) = [0]
[0]
[c_87] = [0]
[0]
[c_88](x1) = [0]
[0]
[c_89] = [0]
[0]
[c_90](x1) = [0]
[0]
[c_91] = [0]
[0]
[#natsub^#](x1, x2) = [0]
[0]
[c_92] = [0]
[0]
[c_93](x1) = [0]
[0]
[c] = [0]
[0]
[c_1](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_3](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_4](x1) = [1 0] x1 + [0]
[0 0] [0]
This order satisfies following ordering constraints
[#equal(@x, @y)] = [0 0] @x + [0 2] @y + [1]
[0 2] [0 0] [0]
>= [1]
[0]
= [#eq(@x, @y)]
[#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [1]
[0]
>= [1]
[0]
= [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))]
[#eq(::(@x_1, @x_2), nil())] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(nil(), ::(@y_1, @y_2))] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(nil(), nil())] = [1]
[0]
> [0]
[0]
= [#true()]
[#eq(#0(), #0())] = [1]
[0]
> [0]
[0]
= [#true()]
[#eq(#0(), #s(@y))] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(#0(), #neg(@y))] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(#0(), #pos(@y))] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(#s(@x), #0())] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(#s(@x), #s(@y))] = [1]
[0]
>= [1]
[0]
= [#eq(@x, @y)]
[#eq(#neg(@x), #0())] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(#neg(@x), #neg(@y))] = [1]
[0]
>= [1]
[0]
= [#eq(@x, @y)]
[#eq(#neg(@x), #pos(@y))] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(#pos(@x), #0())] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(#pos(@x), #neg(@y))] = [1]
[0]
>= [1]
[0]
= [#false()]
[#eq(#pos(@x), #pos(@y))] = [1]
[0]
>= [1]
[0]
= [#eq(@x, @y)]
[-(@x, @y)] = [1 0] @x + [2]
[2 1] [2]
>= [1 0] @x + [2]
[2 1] [2]
= [#sub(@x, @y)]
[#sub(@x, #0())] = [1 0] @x + [2]
[2 1] [2]
> [1 0] @x + [0]
[0 1] [0]
= [@x]
[#sub(@x, #neg(@y))] = [1 0] @x + [2]
[2 1] [2]
>= [1 0] @x + [2]
[2 1] [2]
= [#add(@x, #pos(@y))]
[#sub(@x, #pos(@y))] = [1 0] @x + [2]
[2 1] [2]
>= [1 0] @x + [2]
[2 1] [2]
= [#add(@x, #neg(@y))]
[filter(@p, @l)] = [1 1] @l + [0]
[0 1] [0]
>= [1 1] @l + [0]
[0 1] [0]
= [filter#1(@l, @p)]
[filter#1(::(@x, @xs), @p)] = [1 0] @x + [1 3] @xs + [1]
[0 0] [0 1] [1]
> [1 0] @x + [1 3] @xs + [0]
[0 0] [0 1] [1]
= [filter#2(filter(@p, @xs), @p, @x)]
[filter#1(nil(), @p)] = [0]
[0]
>= [0]
[0]
= [nil()]
[filter#2(@xs', @p, @x)] = [1 0] @x + [1 2] @xs' + [0]
[0 0] [0 1] [1]
>= [1 0] @x + [1 2] @xs' + [0]
[0 0] [0 1] [1]
= [filter#3(#equal(mod(@x, @p), #0()), @x, @xs')]
[mod(@x, @y)] = [1 0] @x + [2]
[2 1] [2]
>= [1 0] @x + [2]
[2 1] [2]
= [-(@x, *(@y, div(@x, @y)))]
[filter#3(#false(), @x, @xs')] = [1 0] @x + [1 2] @xs' + [0]
[0 0] [0 1] [1]
>= [1 0] @x + [1 2] @xs' + [0]
[0 0] [0 1] [1]
= [::(@x, @xs')]
[filter#3(#true(), @x, @xs')] = [1 0] @x + [1 2] @xs' + [0]
[0 0] [0 1] [0]
>= [1 0] @xs' + [0]
[0 1] [0]
= [@xs']
[#add(#0(), @y)] = [1 0] @y + [3]
[2 1] [4]
> [1 0] @y + [0]
[0 1] [0]
= [@y]
[#add(#neg(#s(#0())), @y)] = [1 0] @y + [2]
[2 1] [2]
>= [2]
[2]
= [#pred(@y)]
[#add(#neg(#s(#s(@x))), @y)] = [1 0] @y + [2]
[2 1] [2]
>= [2]
[2]
= [#pred(#add(#pos(#s(@x)), @y))]
[#add(#pos(#s(#0())), @y)] = [1 0] @y + [2]
[2 1] [2]
>= [0 0] @y + [2]
[1 0] [0]
= [#succ(@y)]
[#add(#pos(#s(#s(@x))), @y)] = [1 0] @y + [2]
[2 1] [2]
>= [0 0] @y + [2]
[1 0] [2]
= [#succ(#add(#pos(#s(@x)), @y))]
[#pred(#0())] = [2]
[2]
> [1]
[0]
= [#neg(#s(#0()))]
[#pred(#neg(#s(@x)))] = [2]
[2]
> [1]
[0]
= [#neg(#s(#s(@x)))]
[#pred(#pos(#s(#0())))] = [2]
[2]
>= [2]
[0]
= [#0()]
[#pred(#pos(#s(#s(@x))))] = [2]
[2]
> [1]
[0]
= [#pos(#s(@x))]
[#succ(#0())] = [2]
[2]
> [1]
[0]
= [#pos(#s(#0()))]
[#succ(#neg(#s(#0())))] = [2]
[1]
>= [2]
[0]
= [#0()]
[#succ(#neg(#s(#s(@x))))] = [2]
[1]
> [1]
[0]
= [#neg(#s(@x))]
[#succ(#pos(#s(@x)))] = [2]
[1]
> [1]
[0]
= [#pos(#s(#s(@x)))]
[#and(#false(), #false())] = [1]
[0]
>= [1]
[0]
= [#false()]
[#and(#false(), #true())] = [1]
[0]
>= [1]
[0]
= [#false()]
[#and(#true(), #false())] = [1]
[0]
>= [1]
[0]
= [#false()]
[#and(#true(), #true())] = [1]
[0]
> [0]
[0]
= [#true()]
[#natdiv(#0(), #0())] = [4]
[2]
> [0]
[0]
= [#divByZero()]
[#natdiv(#0(), #s(@y))] = [4]
[4]
> [2]
[0]
= [#0()]
[#natdiv(#s(@x), #0())] = [2 0] @x + [4]
[0 0] [2]
> [0]
[0]
= [#divByZero()]
[#natdiv(#s(@x), #s(@y))] = [2 0] @x + [4]
[0 0] [4]
>= [2 0] @x + [4]
[0 0] [4]
= [#natdiv'(#divsub(@x, @y), #s(@y))]
[#divsub(#0(), #0())] = [3]
[3]
> [2]
[0]
= [#0()]
[#divsub(#0(), #s(@y))] = [0 0] @y + [3]
[1 0] [3]
> [0]
[0]
= [#underflow()]
[#divsub(#s(@x), #0())] = [1 0] @x + [3]
[0 0] [3]
> [1 0] @x + [2]
[0 0] [1]
= [#s(@x)]
[#divsub(#s(@x), #s(@y))] = [1 0] @x + [0 0] @y + [3]
[0 0] [1 0] [3]
> [1 0] @x + [0 0] @y + [1]
[0 0] [1 0] [1]
= [#divsub(@x, @y)]
[#natdiv'(#0(), @y)] = [0 0] @y + [6]
[0 2] [2]
> [4]
[1]
= [#s(#0())]
[#natdiv'(#s(@x), @y)] = [2 0] @x + [0 0] @y + [6]
[0 0] [0 2] [2]
>= [2 0] @x + [6]
[0 0] [1]
= [#s(#natdiv(#s(@x), @y))]
[#natdiv'(#underflow(), @y)] = [0 0] @y + [2]
[0 2] [2]
>= [2]
[0]
= [#0()]
[eratos^#(@l)] = [2 0] @l + [1]
[1 1] [0]
>= [2 0] @l + [1]
[0 0] [0]
= [c_1(eratos#1^#(@l))]
[eratos#1^#(::(@x, @xs))] = [2 0] @x + [2 4] @xs + [1]
[0 0] [0 0] [0]
>= [2 4] @xs + [1]
[0 0] [0]
= [c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))]
[filter^#(@p, @l)] = [0 2] @l + [0]
[1 0] [2]
>= [0 2] @l + [0]
[0 0] [0]
= [c_3(filter#1^#(@l, @p))]
[filter#1^#(::(@x, @xs), @p)] = [0 2] @xs + [2]
[0 0] [0]
> [0 2] @xs + [0]
[0 0] [0]
= [c_4(filter^#(@p, @xs))]
The strictly oriented rules are moved into the corresponding weak
component(s).
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ eratos^#(@l) -> c_1(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) }
Weak DPs: { filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 1: eratos^#(@l) -> c_1(eratos#1^#(@l))
, 4: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) }
Trs:
{ #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, #sub(@x, #0()) -> @x
, #div(#0(), #0()) -> #divByZero()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #pred(#pos(#s(#0()))) -> #0()
, #and(#true(), #true()) -> #true() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
Uargs(c_4) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#equal](x1, x2) = [0 1] x2 + [0]
[0 1] [0]
[#eq](x1, x2) = [0 1] x2 + [0]
[0 1] [0]
[*](x1, x2) = [2 1] x2 + [0]
[1 0] [0]
[#mult](x1, x2) = [2]
[0]
[-](x1, x2) = [2 0] x1 + [1 0] x2 + [0]
[0 1] [1 0] [0]
[#sub](x1, x2) = [2 0] x1 + [1 0] x2 + [0]
[2 2] [0 2] [2]
[div](x1, x2) = [0 1] x1 + [0]
[0 1] [0]
[#div](x1, x2) = [1]
[0]
[eratos](x1) = [0]
[0]
[eratos#1](x1) = [0]
[0]
[::](x1, x2) = [1 0] x2 + [2]
[1 1] [2]
[filter](x1, x2) = [1 0] x2 + [0]
[0 1] [1]
[nil] = [0]
[1]
[filter#1](x1, x2) = [1 0] x1 + [0]
[0 1] [1]
[filter#2](x1, x2, x3) = [1 0] x1 + [2]
[1 1] [2]
[mod](x1, x2) = [0 0] x1 + [0]
[1 1] [0]
[#0] = [2]
[1]
[filter#3](x1, x2, x3) = [1 1] x1 + [1 0] x3 + [0]
[0 2] [1 1] [0]
[#false] = [1]
[1]
[#true] = [0]
[1]
[#add](x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [1 0] [0]
[#s](x1) = [1 0] x1 + [1]
[0 1] [1]
[#neg](x1) = [0 0] x1 + [1]
[0 1] [2]
[#pred](x1) = [1 0] x1 + [0]
[0 0] [1]
[#pos](x1) = [1 0] x1 + [1]
[0 1] [2]
[#succ](x1) = [2]
[2]
[#and](x1, x2) = [0 0] x2 + [1]
[0 1] [0]
[#divByZero] = [0]
[0]
[#natdiv](x1, x2) = [0]
[0]
[#positive](x1) = [2 0] x1 + [1]
[0 0] [0]
[#negative](x1) = [2 0] x1 + [0]
[0 0] [0]
[#divsub](x1, x2) = [0]
[0]
[#underflow] = [0]
[0]
[#natmult](x1, x2) = [0 2] x2 + [0]
[2 2] [0]
[#natadd](x1, x2) = [1 1] x2 + [0]
[2 1] [1]
[#natdiv'](x1, x2) = [0]
[0]
[#natsub](x1, x2) = [0]
[0]
[#equal^#](x1, x2) = [0]
[0]
[c_1](x1) = [0]
[0]
[#eq^#](x1, x2) = [0]
[0]
[*^#](x1, x2) = [0]
[0]
[c_2](x1) = [0]
[0]
[#mult^#](x1, x2) = [0]
[0]
[-^#](x1, x2) = [0]
[0]
[c_3](x1) = [0]
[0]
[#sub^#](x1, x2) = [0]
[0]
[div^#](x1, x2) = [0]
[0]
[c_4](x1) = [0]
[0]
[#div^#](x1, x2) = [0]
[0]
[eratos^#](x1) = [1 1] x1 + [1]
[0 0] [0]
[c_5](x1) = [0]
[0]
[eratos#1^#](x1) = [1 1] x1 + [0]
[0 0] [0]
[c_6](x1, x2) = [0]
[0]
[filter^#](x1, x2) = [1 0] x2 + [2]
[0 0] [0]
[c_7] = [0]
[0]
[c_8](x1) = [0]
[0]
[filter#1^#](x1, x2) = [1 0] x1 + [1]
[0 0] [0]
[c_9](x1, x2) = [0]
[0]
[filter#2^#](x1, x2, x3) = [0]
[0]
[c_10] = [0]
[0]
[c_11](x1, x2, x3) = [0]
[0]
[filter#3^#](x1, x2, x3) = [0]
[0]
[mod^#](x1, x2) = [0]
[0]
[c_12](x1, x2, x3) = [0]
[0]
[c_13] = [0]
[0]
[c_14] = [0]
[0]
[c_15](x1, x2, x3) = [0]
[0]
[#and^#](x1, x2) = [0]
[0]
[c_16] = [0]
[0]
[c_17] = [0]
[0]
[c_18] = [0]
[0]
[c_19] = [0]
[0]
[c_20] = [0]
[0]
[c_21] = [0]
[0]
[c_22] = [0]
[0]
[c_23] = [0]
[0]
[c_24](x1) = [0]
[0]
[c_25] = [0]
[0]
[c_26](x1) = [0]
[0]
[c_27] = [0]
[0]
[c_28] = [0]
[0]
[c_29] = [0]
[0]
[c_30](x1) = [0]
[0]
[c_31] = [0]
[0]
[c_32] = [0]
[0]
[c_33] = [0]
[0]
[c_34] = [0]
[0]
[c_35](x1) = [0]
[0]
[#natmult^#](x1, x2) = [0]
[0]
[c_36](x1) = [0]
[0]
[c_37] = [0]
[0]
[c_38](x1) = [0]
[0]
[c_39](x1) = [0]
[0]
[c_40] = [0]
[0]
[c_41](x1) = [0]
[0]
[#add^#](x1, x2) = [0]
[0]
[c_42](x1) = [0]
[0]
[c_43] = [0]
[0]
[c_44] = [0]
[0]
[c_45] = [0]
[0]
[c_46] = [0]
[0]
[c_47](x1, x2) = [0]
[0]
[#positive^#](x1) = [0]
[0]
[#natdiv^#](x1, x2) = [0]
[0]
[c_48](x1, x2) = [0]
[0]
[#negative^#](x1) = [0]
[0]
[c_49] = [0]
[0]
[c_50](x1, x2) = [0]
[0]
[c_51](x1, x2) = [0]
[0]
[c_52] = [0]
[0]
[c_53](x1) = [0]
[0]
[#pred^#](x1) = [0]
[0]
[c_54](x1, x2) = [0]
[0]
[c_55](x1) = [0]
[0]
[#succ^#](x1) = [0]
[0]
[c_56](x1, x2) = [0]
[0]
[c_57] = [0]
[0]
[c_58] = [0]
[0]
[c_59] = [0]
[0]
[c_60] = [0]
[0]
[c_61] = [0]
[0]
[c_62] = [0]
[0]
[c_63] = [0]
[0]
[c_64] = [0]
[0]
[c_65] = [0]
[0]
[c_66] = [0]
[0]
[c_67] = [0]
[0]
[c_68] = [0]
[0]
[c_69] = [0]
[0]
[c_70] = [0]
[0]
[c_71] = [0]
[0]
[c_72](x1, x2) = [0]
[0]
[#natdiv'^#](x1, x2) = [0]
[0]
[#divsub^#](x1, x2) = [0]
[0]
[c_73] = [0]
[0]
[c_74] = [0]
[0]
[c_75] = [0]
[0]
[c_76] = [0]
[0]
[c_77] = [0]
[0]
[c_78] = [0]
[0]
[c_79] = [0]
[0]
[c_80] = [0]
[0]
[c_81] = [0]
[0]
[c_82] = [0]
[0]
[c_83] = [0]
[0]
[c_84](x1) = [0]
[0]
[c_85] = [0]
[0]
[c_86](x1, x2) = [0]
[0]
[#natadd^#](x1, x2) = [0]
[0]
[c_87] = [0]
[0]
[c_88](x1) = [0]
[0]
[c_89] = [0]
[0]
[c_90](x1) = [0]
[0]
[c_91] = [0]
[0]
[#natsub^#](x1, x2) = [0]
[0]
[c_92] = [0]
[0]
[c_93](x1) = [0]
[0]
[c] = [0]
[0]
[c_1](x1) = [1 1] x1 + [0]
[0 0] [0]
[c_2](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_3](x1) = [1 1] x1 + [1]
[0 0] [0]
[c_4](x1) = [1 1] x1 + [0]
[0 0] [0]
This order satisfies following ordering constraints
[#equal(@x, @y)] = [0 1] @y + [0]
[0 1] [0]
>= [0 1] @y + [0]
[0 1] [0]
= [#eq(@x, @y)]
[#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [1 1] @y_2 + [2]
[1 1] [2]
> [0 0] @y_2 + [1]
[0 1] [0]
= [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))]
[#eq(::(@x_1, @x_2), nil())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#eq(nil(), ::(@y_1, @y_2))] = [1 1] @y_2 + [2]
[1 1] [2]
> [1]
[1]
= [#false()]
[#eq(nil(), nil())] = [1]
[1]
> [0]
[1]
= [#true()]
[#eq(#0(), #0())] = [1]
[1]
> [0]
[1]
= [#true()]
[#eq(#0(), #s(@y))] = [0 1] @y + [1]
[0 1] [1]
>= [1]
[1]
= [#false()]
[#eq(#0(), #neg(@y))] = [0 1] @y + [2]
[0 1] [2]
> [1]
[1]
= [#false()]
[#eq(#0(), #pos(@y))] = [0 1] @y + [2]
[0 1] [2]
> [1]
[1]
= [#false()]
[#eq(#s(@x), #0())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#eq(#s(@x), #s(@y))] = [0 1] @y + [1]
[0 1] [1]
> [0 1] @y + [0]
[0 1] [0]
= [#eq(@x, @y)]
[#eq(#neg(@x), #0())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#eq(#neg(@x), #neg(@y))] = [0 1] @y + [2]
[0 1] [2]
> [0 1] @y + [0]
[0 1] [0]
= [#eq(@x, @y)]
[#eq(#neg(@x), #pos(@y))] = [0 1] @y + [2]
[0 1] [2]
> [1]
[1]
= [#false()]
[#eq(#pos(@x), #0())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#eq(#pos(@x), #neg(@y))] = [0 1] @y + [2]
[0 1] [2]
> [1]
[1]
= [#false()]
[#eq(#pos(@x), #pos(@y))] = [0 1] @y + [2]
[0 1] [2]
> [0 1] @y + [0]
[0 1] [0]
= [#eq(@x, @y)]
[filter(@p, @l)] = [1 0] @l + [0]
[0 1] [1]
>= [1 0] @l + [0]
[0 1] [1]
= [filter#1(@l, @p)]
[filter#1(::(@x, @xs), @p)] = [1 0] @xs + [2]
[1 1] [3]
>= [1 0] @xs + [2]
[1 1] [3]
= [filter#2(filter(@p, @xs), @p, @x)]
[filter#1(nil(), @p)] = [0]
[2]
>= [0]
[1]
= [nil()]
[filter#2(@xs', @p, @x)] = [1 0] @xs' + [2]
[1 1] [2]
>= [1 0] @xs' + [2]
[1 1] [2]
= [filter#3(#equal(mod(@x, @p), #0()), @x, @xs')]
[filter#3(#false(), @x, @xs')] = [1 0] @xs' + [2]
[1 1] [2]
>= [1 0] @xs' + [2]
[1 1] [2]
= [::(@x, @xs')]
[filter#3(#true(), @x, @xs')] = [1 0] @xs' + [1]
[1 1] [2]
> [1 0] @xs' + [0]
[0 1] [0]
= [@xs']
[#and(#false(), #false())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#and(#false(), #true())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#and(#true(), #false())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#and(#true(), #true())] = [1]
[1]
> [0]
[1]
= [#true()]
[eratos^#(@l)] = [1 1] @l + [1]
[0 0] [0]
> [1 1] @l + [0]
[0 0] [0]
= [c_1(eratos#1^#(@l))]
[eratos#1^#(::(@x, @xs))] = [2 1] @xs + [4]
[0 0] [0]
>= [2 1] @xs + [4]
[0 0] [0]
= [c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))]
[filter^#(@p, @l)] = [1 0] @l + [2]
[0 0] [0]
>= [1 0] @l + [2]
[0 0] [0]
= [c_3(filter#1^#(@l, @p))]
[filter#1^#(::(@x, @xs), @p)] = [1 0] @xs + [3]
[0 0] [0]
> [1 0] @xs + [2]
[0 0] [0]
= [c_4(filter^#(@p, @xs))]
Consider the set of all dependency pairs
DPs:
{ 1: eratos^#(@l) -> c_1(eratos#1^#(@l))
, 2: eratos#1^#(::(@x, @xs)) ->
c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, 3: filter^#(@p, @l) -> c_3(filter#1^#(@l, @p))
, 4: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) }
Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of dependency
pairs {1,4}. These cover all (indirect) predecessors of dependency
pairs {1,2,3,4}, their number of application is equally bounded.
The dependency pairs are shifted into the corresponding weak
component(s).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ eratos^#(@l) -> c_1(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, filter^#(@p, @l) -> c_3(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) }
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0() }
StartTerms: basic terms
Strategy: innermost
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ eratos^#(@l) -> c_1(eratos#1^#(@l))
, eratos#1^#(::(@x, @xs)) ->
c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))
, filter^#(@p, @l) -> c_3(filter#1^#(@l, @p))
, filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
, #eq(::(@x_1, @x_2), nil()) -> #false()
, #eq(nil(), ::(@y_1, @y_2)) -> #false()
, #eq(nil(), nil()) -> #true()
, #eq(#0(), #0()) -> #true()
, #eq(#0(), #s(@y)) -> #false()
, #eq(#0(), #neg(@y)) -> #false()
, #eq(#0(), #pos(@y)) -> #false()
, #eq(#s(@x), #0()) -> #false()
, #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #0()) -> #false()
, #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
, #eq(#neg(@x), #pos(@y)) -> #false()
, #eq(#pos(@x), #0()) -> #false()
, #eq(#pos(@x), #neg(@y)) -> #false()
, #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
, *(@x, @y) -> #mult(@x, @y)
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, -(@x, @y) -> #sub(@x, @y)
, #sub(@x, #0()) -> @x
, #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
, #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
, div(@x, @y) -> #div(@x, @y)
, #div(#0(), #0()) -> #divByZero()
, #div(#0(), #neg(@y)) -> #0()
, #div(#0(), #pos(@y)) -> #0()
, #div(#neg(@x), #0()) -> #divByZero()
, #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
, #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #0()) -> #divByZero()
, #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
, #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
, filter(@p, @l) -> filter#1(@l, @p)
, filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
, filter#1(nil(), @p) -> nil()
, filter#2(@xs', @p, @x) ->
filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
, mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
, filter#3(#false(), @x, @xs') -> ::(@x, @xs')
, filter#3(#true(), @x, @xs') -> @xs'
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #and(#false(), #false()) -> #false()
, #and(#false(), #true()) -> #false()
, #and(#true(), #false()) -> #false()
, #and(#true(), #true()) -> #true()
, #natdiv(#0(), #0()) -> #divByZero()
, #natdiv(#0(), #s(@y)) -> #0()
, #natdiv(#s(@x), #0()) -> #divByZero()
, #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
, #positive(#0()) -> #0()
, #positive(#s(@x)) -> #pos(#s(@x))
, #positive(#neg(@x)) -> #neg(@x)
, #positive(#pos(@x)) -> #pos(@x)
, #negative(#0()) -> #0()
, #negative(#s(@x)) -> #neg(#s(@x))
, #negative(#neg(@x)) -> #pos(@x)
, #negative(#pos(@x)) -> #neg(@x)
, #divsub(#0(), #0()) -> #0()
, #divsub(#0(), #s(@y)) -> #underflow()
, #divsub(#s(@x), #0()) -> #s(@x)
, #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
, #natadd(#0(), @y) -> @y
, #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
, #natdiv'(#0(), @y) -> #s(#0())
, #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
, #natdiv'(#underflow(), @y) -> #0() }
StartTerms: basic terms
Strategy: innermost
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))